($\lambda$$T$,$L_{1}$,$L_{2}$,$z$. $L_{1}$ $\subseteq$ $L_{2}$) $\in$ $T$:Type$\rightarrow$($T$ List)$\rightarrow$($T$ List)$\rightarrow\downarrow$True$\rightarrow$Prop